FDL - Step of Proof: nat_well_founded

Step of Proof: nat_well_founded

Inference at *
Iof proof for Lemma nat well founded:

WellFnd{i}(

;x,y.x < y)

by UnfoldTopAb 0

1:

1:

P:(

). (

j:

. (

k:

. (k < j)

P(k))

P(j))

{

n:

. P(n)}

.

Definitions WellFnd{i}(A;x,y.R(x;y))